/*
 * FalseEscWarningMultiply.java
 * 
 * Copyright 2008 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.examples;

/**
 * @author csallner@gatech.edu (Christoph Csallner)
 */
public class FalseEscWarningMultiply {

	/**
	 * ESC/Java makes conservative assumptions for multiplications. 
	 * Here it assumes (p^2 = -1) and produces a bogus 
	 * division by zero warning.
	 */
	public int noBug(int p) {
		if (p < -1000 || p > 1000)	//rule out int overflow
			return 0;
		
		p = p*p + 1;	//makes p larger than zero
		return 1000/p;
	}
	
	
	/**
	 * Similar, muliplication always 0*0
	 */
	public int noBugSimple(int p) {
		if (p!=0)
			return 0;
		
		p = p*p + 1;	//p==1
		return 1000/p;
	}

}
